// SPDX-FileCopyrightText: 2023-2025 CASTest Corporation Limited
// SPDX-FileCopyrightText: 2023-2025 Institute of Computing Technology, Chinese Academy of Sciences
// SPDX-License-Identifier: LGPL-v3

#include "atpg/SAFTest.h"

namespace ictest {

void SAFTest::InitSAFTestStatus() {
  good_.assign(prim_->NumGates(), LOGIC_x);
  bad_.assign(prim_->NumGates(), LOGIC_x);
  atpg_constrain_value_.assign(prim_->NumGates(), LOGIC_x);
  backtracks_ = 0;
  total_backtracks_ = 0;
  max_backtracks_ = 0;
  atpg_invokes_ = 0;
  fault_observed_ = false;

  dec_tree_ = new SplitDecisionTree();
  dec_stack_.clear();
  driven_table_ = new LogicDrivenTable(prim_);
  fault_cone_.assign(prim_->NumGates(), -1);

  is_observe_gate_.assign(prim_->NumGates(), false);
  is_ppi_.assign(prim_->NumGates(), false);
  for (int i = 0; i < prim_->ScanChains().size(); ++i) {
    for (int j = 0; j < prim_->ScanChains()[i]->ScanChainDFFs().size(); ++j) {
      Gate *sc_dff = prim_->ScanChains()[i]->ScanChainDFFs()[j];
      gate2scanchainid_.insert(std::make_pair(sc_dff, i));
      is_ppi_[sc_dff->GetGId()] = true;
      for (const auto &fanin : sc_dff->FaninGates()) {
        is_observe_gate_[fanin->GetGId()] = true;
      }
    }
  }
  for (const auto &po : prim_->GetPOGates()) {
    is_observe_gate_[po->GetGId()] = true;
  }

  no_assign_.assign(prim_->NumGates(), false);
  MarkClkCone();
  GetRegisterInfo();
  for (const auto &tie_gate : prim_->GetTieGates()) {
    if (tie_gate->GetGType() == GType::G_TIEX ||
        tie_gate->GetGType() == GType::G_TIEZ) {
      no_assign_[tie_gate->GetGId()] = true;
    }
  }
  for (const auto &nsc_dff : prim_->GetNonScanDFFGates()) {
    no_assign_[nsc_dff->GetGId()] = true;
  }

  FindFreeFanoutRegion();
  fault_support_region_.resize(free_fanout_regions_.size(), -1);
  already_visited_ffr_.resize(free_fanout_regions_.size(), -1);

  ImplyATPGConstraints();
}

// 约束的蕴含
void SAFTest::ImplyATPGConstraints() {
  pre_imply_ = true;
  std::vector<Gate *> manda_imply_good, manda_imply_bad;
  std::vector<std::pair<Gate *, uint8_t>> uj_good, uj_bad;
  for (int i = 0; i < prim_->GetTieGates().size(); i++) {
    if (prim_->GetTieGates()[i]->GetGType() == GType::G_TIE0) {
      good_[prim_->GetTieGates()[i]->GetGId()] = LOGIC_0;
    } else if (prim_->GetTieGates()[i]->GetGType() == GType::G_TIE1) {
      good_[prim_->GetTieGates()[i]->GetGId()] = LOGIC_1;
    }

    if (prim_->GetTieGates()[i]->GetGType() != GType::G_TIEX) {
      manda_imply_good.emplace_back(prim_->GetTieGates()[i]);
    }
  }

  for (auto &tm : prim_->GetTM2Values()) {
    good_[tm.first] = static_cast<int>(tm.second);
    manda_imply_good.emplace_back(prim_->GetPrimNetlist()[tm.first]);
  }

  if (!Imply(manda_imply_good, manda_imply_bad, uj_good, uj_bad)) {
    LOG_INFO("Error! cant not meet mandatory imply")
    assert(false);
  }
  for (int i = 0; i < good_.size(); i++) {
    atpg_constrain_value_[i] = good_[i];
  }
  pre_imply_ = false;
}

void SAFTest::ResetSAFTestStatus() {
  backtracks_ = 0;
  atpg_invokes_++;
  fault_observed_ = false;

  good_.assign(prim_->NumGates(), LOGIC_x);
  good_ = atpg_constrain_value_;
  bad_.assign(prim_->NumGates(), LOGIC_x);

  dec_stack_.clear();
  if (dec_tree_->get_root()->child_) {
    dec_tree_->delete_silb_child(dec_tree_->get_root()->child_);
  }
  dec_tree_->get_root()->child_ = nullptr;
  dec_tree_->get_root()->done_dec();
}

void SAFTest::MarkFaultCone() {
  std::queue<Gate *> que;
  que.push(faulty_gate_);
  fault_cone_[faulty_gate_->GetGId()] = atpg_invokes_;

  while (!que.empty()) {
    auto gate = que.front();
    que.pop();
    if (is_observe_gate_[gate->GetGId()]) {
      continue;
    }
    for (auto fanout : gate->FanoutGates()) {
      if (OutFaultCone(fanout->GetGId()) &&
          !is_seq_element_[fanout->GetGId()]) {
        que.push(fanout);
        fault_cone_[fanout->GetGId()] = atpg_invokes_;
      }
    }
  }
}

// 搜索support region
void SAFTest::FindFaultSupportRegion() {
  int ffr_id = gate_ffr_id_[faulty_gate_->GetGId()];
  FreeFanoutRegion *ffr = free_fanout_regions_[ffr_id];
  std::queue<FreeFanoutRegion *> que;
  std::queue<FreeFanoutRegion *> po_que;
  que.push(ffr);
  already_visited_ffr_[ffr->id] = atpg_invokes_;

  while (!que.empty()) {
    ffr = que.front();
    que.pop();

    if (is_observe_gate_[ffr->stem->GetGId()]) {
      if (ffr->stem->FanoutSize() > 0) {
        for (auto fanin : ffr->stem->FanoutGates()[0]->FaninGates()) {
          auto fanin_ffr = free_fanout_regions_[gate_ffr_id_[fanin->GetGId()]];
          if (fault_support_region_[fanin_ffr->id] != atpg_invokes_) {
            po_que.emplace(fanin_ffr);
            fault_support_region_[fanin_ffr->id] = atpg_invokes_;
          }
        }
      } else {
        if (fault_support_region_[ffr->id] != atpg_invokes_) {
          po_que.emplace(ffr);
          fault_support_region_[ffr->id] = atpg_invokes_;
        }
      }
    }

    if ((!ffr->fanouts.empty()) &&
        ffr->stem->FanoutGates()[0]->GetGType() == GType::G_DFF &&
        gate2scanchainid_.count(ffr->stem->FanoutGates()[0])) {
      continue;
    }

    for (auto fanout : ffr->fanouts) {
      if (already_visited_ffr_[fanout->id] != atpg_invokes_ &&
          fanout->stem->GetGType() != GType::G_DFF) {
        already_visited_ffr_[fanout->id] = atpg_invokes_;
        que.push(fanout);
      }
    }
  }

  while (!po_que.empty()) {
    ffr = po_que.front();
    po_que.pop();
    for (auto fanin : ffr->fanins) {
      if (fault_support_region_[fanin->id] != atpg_invokes_) {
        fault_support_region_[fanin->id] = atpg_invokes_;
        po_que.push(fanin);
      }
    }
  }
}

bool SAFTest::InjectFaultEffectAndMandatory() {
  int faulty_val =
      fault_under_test_->GetSAFType() == SAFType::SA0 ? LOGIC_S1 : LOGIC_S0;
  std::vector<Gate *> manda_imply_good, manda_imply_bad;
  std::vector<std::pair<Gate *, uint8_t>> uj_good, uj_bad;

  if (faulty_gate_->GetGType() == GType::G_TIE0 ||
      good_[faulty_gate_->GetGId()] == LOGIC_0) {
    if (faulty_val == LOGIC_S1) {
      return false;
    }
  } else if (faulty_gate_->GetGType() == GType::G_TIE1 ||
             good_[faulty_gate_->GetGId()] == LOGIC_1) {
    if (faulty_val == LOGIC_S0) {
      return false;
    }
  }

  // UNIQUE SENSITIZATION for faulty gate is necessary!
  // For single path oriented segment, sensitize FFR of faulty gate.
  if (faulty_gate_->FanoutSize() == 1) {
    Gate *fault_path = faulty_gate_;
    Gate *dominator = faulty_gate_->FanoutGates()[0];
    while (true) {
      if (static_cast<int>(dominator->GetNonCtrInVal()) != LOGIC_x &&
          dominator->FaninSize() > 1) {
        for (auto fanin : dominator->FaninGates()) {
          if (fanin != fault_path) {
            if (deter_val(good_[fanin->GetGId()]) &&
                good_[fanin->GetGId()] !=
                    static_cast<int>(dominator->GetNonCtrInVal())) {
              ResetImply(manda_imply_good, manda_imply_bad);
              return false;
            } else if (unknown_val(good_[fanin->GetGId()])) {
              if (no_assign_[fanin->GetGId()]) {
                ResetImply(manda_imply_good, manda_imply_bad);
                return false;
              }
              good_[fanin->GetGId()] =
                  static_cast<int>(dominator->GetNonCtrInVal());
              manda_imply_good.emplace_back(fanin);
            }
          }
        }
      }
      if (dominator->FanoutSize() == 1) {
        fault_path = dominator;
        dominator = dominator->FanoutGates()[0];
      } else {
        break;
      }
    }
  }

  // Preprocess fault site.
  // 1. Justify the faulty gate.
  // 2. Gather the first path-segments.

  if (deter_val(good_[faulty_gate_->GetGId()]) &&
      good_[faulty_gate_->GetGId()] != GOOD_VALUE[faulty_val]) {
    ResetImply(manda_imply_good, manda_imply_bad);
    return false;
  } else if (unknown_val(good_[faulty_gate_->GetGId()])) {
    good_[faulty_gate_->GetGId()] = GOOD_VALUE[faulty_val];
    manda_imply_good.emplace_back(faulty_gate_);
  }

  MarkFaultCone();
  FindFaultSupportRegion();

  assert(bad_[faulty_gate_->GetGId()] == LOGIC_x);
  bad_[faulty_gate_->GetGId()] = BAD_VALUE[faulty_val];
  manda_imply_bad.emplace_back(faulty_gate_);

  if (!Imply(manda_imply_good, manda_imply_bad, uj_good, uj_bad)) {
    ResetImply(manda_imply_good, manda_imply_bad);
    return false;
  }

  // Create decision node and add to root's children.
  // Do justification after sibling propagation.
  EliminateUnjustified(uj_good, true);
  EliminateUnjustified(uj_bad, false);
  AddToChildrenPropagation(dec_tree_->get_root(), faulty_gate_);
  AddToChildrenUnjustified(dec_tree_->get_root(), uj_good, uj_bad);

  dec_tree_->get_root()->set_imply(manda_imply_good, manda_imply_bad);
  return true;
}

int SAFTest::TestGen(SAF *target_fault, int max_allowed_backtracks) {

  int status = NO_TEST;
  max_allowed_backtracks_ = max_allowed_backtracks;
  fault_under_test_ = target_fault;
  faulty_gate_ = target_fault->GetSAFGate();

  ResetSAFTestStatus();

  if (!InjectFaultEffectAndMandatory()) {
    return NO_TEST;
  }

  while (true) {

    bool success = false;
    auto dec_node = dec_tree_->next_dec();

    if (!dec_node) {
      status = TEST_FOUND;
      break;
    } else {
      if (!dec_node->initialized()) {
        dec_stack_.emplace_back(dec_node);
      }
      success = MakeDecision(dec_node);
    }
    if (!success) {
      if (backtracks_ > max_allowed_backtracks_) {
        status = OVER_BACKTRACK;
        break;
      }
      backtracks_++;
      if (!Backtrack()) {
        status = NO_TEST;
        break;
      }
    }
  }

  if (status != OVER_BACKTRACK) {
    max_backtracks_ = std::max(max_backtracks_, backtracks_);
  }
  total_backtracks_ += backtracks_;

  return status;
}

bool SAFTest::MakeDecision(SplitSiblingTreeNode *dec_node) {
  bool possible = true;
  std::vector<Gate *> good_imply;
  std::vector<Gate *> bad_imply;
  std::vector<std::pair<Gate *, uint8_t>> unjustified_good;
  std::vector<std::pair<Gate *, uint8_t>> unjustified_bad;

  // If decision node is PROPAGATION.
  // Propagation make both good and bad decisions.
  // Decision are only made at transitive fanout
  // of last propagation decision.
  if (dec_node->dec_type() == PROPAGATION) {
    std::pair<Gate *, Gate *> chosen_path;
    auto prop_node = dynamic_cast<SplitPropagationNode *>(dec_node);
    std::vector<std::pair<Gate *, Gate *>> ppath;

    // If propagation node is not initialized,
    // calculate all possible propagation decisions at current state.
    if (!prop_node->initialized()) {
      ppath = PathOfTransitiveFanout(prop_node->gate_);
      prop_node->set_dec_paths(ppath);
      prop_node->calc_propagation(driven_table_, gate2scanchainid_, good_, bad_,
                                  fault_cone_, atpg_invokes_,
                                  is_falling_edge_dff_, no_assign_);
    }

    std::vector<std::pair<Gate *, int>> justify_objs;
    if (prop_node->another_dec() && !fault_observed_) {
      justify_objs = prop_node->best_path(chosen_path);
      for (auto obj : justify_objs) {
        if (OutFaultCone(obj.first->GetGId())) {
          assert(!(deter_val(good_[obj.first->GetGId()]) &&
                   deter_val(bad_[obj.first->GetGId()]) &&
                   good_[obj.first->GetGId()] != bad_[obj.first->GetGId()]));
        }

        if (OutFaultCone(obj.first->GetGId()) && faulty_val(obj.second)) {
          possible = false;
          break;
        }

        if (GOOD_VALUE[obj.second] != LOGIC_x) {

          assert(good_[obj.first->GetGId()] == LOGIC_x);
          good_[obj.first->GetGId()] = GOOD_VALUE[obj.second];
          good_imply.emplace_back(obj.first);
        }

        if (BAD_VALUE[obj.second] != LOGIC_x) {
          assert(bad_[obj.first->GetGId()] == LOGIC_x);
          if (!OutFaultCone(obj.first->GetGId())) {
            assert(bad_[obj.first->GetGId()] == LOGIC_x);
            bad_[obj.first->GetGId()] = BAD_VALUE[obj.second];
            bad_imply.emplace_back(obj.first);
          } else {
            if (good_[obj.first->GetGId()] == LOGIC_x) {
              good_[obj.first->GetGId()] = BAD_VALUE[obj.second];
              good_imply.emplace_back(obj.first);
            } else if (good_[obj.first->GetGId()] != BAD_VALUE[obj.second]) {
              possible = false;
            }
          }
        }
      }
    } else {
      if (!fault_observed_) {
        possible = false;
      }
    }

    if (possible &&
        !Imply(good_imply, bad_imply, unjustified_good, unjustified_bad)) {
      possible = false;
    }
    // Get next propagation dec node,
    // trace the propagation path of
    // chosen transitive fanout.
    if (possible) {
      if (chosen_path.first && is_ppi_[chosen_path.second->GetGId()]) {
        fault_observed_ = true;
      }
      EliminateUnjustified(unjustified_good, true);
      EliminateUnjustified(unjustified_bad, false);
      if (!fault_observed_) {
        AddToChildrenPropagation(prop_node, chosen_path.second);
      }
      AddToChildrenUnjustified(prop_node, unjustified_good, unjustified_bad);
      AddImplicationsToNode(good_imply, bad_imply, prop_node);
      prop_node->done_dec();
    } else {
      ResetImply(good_imply, bad_imply);
      prop_node->undone_dec();
    }
    // No matter the node is done or not,
    // add this node to decision stack.
  }
  // If decision node is GOOD_JUSTIFY or BAD_JUSTIFY.
  // make decision and construct JUSTIFY nodes,
  // Set all new JUSTIFY nodes as its children.
  else if (dec_node->dec_type() == GOOD_JUSTIFY ||
           dec_node->dec_type() == BAD_JUSTIFY) {
    auto justify_node = dynamic_cast<SplitJustifyNode *>(dec_node);
    if (!justify_node->initialized()) {
      justify_node->calc_justify(driven_table_, gate2scanchainid_, good_, bad_,
                                 fault_cone_, atpg_invokes_,
                                 is_falling_edge_dff_, no_assign_);
    }
    std::vector<std::pair<Gate *, int>> justify_objs;
    if (justify_node->another_dec()) {
      justify_objs = justify_node->best_cube();
      if (justify_node->dec_type() == GOOD_JUSTIFY) {
        for (auto obj : justify_objs) {
          if (obj.second != LOGIC_x) {
            assert(good_[obj.first->GetGId()] == LOGIC_x);
            good_[obj.first->GetGId()] = obj.second;
            good_imply.emplace_back(obj.first);
          }
        }
      } else if (justify_node->dec_type() == BAD_JUSTIFY) {
        for (auto obj : justify_objs) {
          if (obj.second != LOGIC_x) {
            assert(bad_[obj.first->GetGId()] == LOGIC_x);
            if (!OutFaultCone(obj.first->GetGId())) {
              bad_[obj.first->GetGId()] = obj.second;
              bad_imply.emplace_back(obj.first);
            } else {
              if (good_[obj.first->GetGId()] == LOGIC_x) {
                good_[obj.first->GetGId()] = obj.second;
                good_imply.emplace_back(obj.first);
              } else if (good_[obj.first->GetGId()] != obj.second) {
                possible = false;
                break;
              }
            }
          }
        }
      } else {
        assert(false);
      }
    } else {
      uint8_t eval = LOGIC_x;

      if (dec_node->dec_type() == GOOD_JUSTIFY) {
        eval = EvalGate(dec_node->gate_, true);
      } else if (dec_node->dec_type() == BAD_JUSTIFY) {
        eval = EvalGate(dec_node->gate_, false);
      }

      if (eval != dec_node->val_) {
        possible = false;
      }
    }

    if (possible &&
        !Imply(good_imply, bad_imply, unjustified_good, unjustified_bad)) {
      possible = false;
    }

    if (possible) {
      EliminateUnjustified(unjustified_good, true);
      EliminateUnjustified(unjustified_bad, false);
      AddToChildrenUnjustified(justify_node, unjustified_good, unjustified_bad);
      justify_node->done_dec();
      AddImplicationsToNode(good_imply, bad_imply, justify_node);
    } else {
      ResetImply(good_imply, bad_imply);
      justify_node->undone_dec();
    }
    // No matter the node is done or not,
    // add this node to decision stack.
  } else {
    assert(false);
  }

  // If no decision made at current node,
  // and no other possible decisions,
  // Backtrack.
  if (!dec_node->done() && !dec_node->another_dec()) {
    backtracks_++;
    if (backtracks_ > max_allowed_backtracks_) {
      return false;
    } else {
      if (!Backtrack()) {
        return false;
      }
    }
  }
  return true;
}

bool SAFTest::Backtrack() {

  std::vector<Gate *> imply_good, imply_bad;
  // If decision stack is not empty, try to Backtrack.

  while (!dec_stack_.empty()) {
    auto dec = dec_stack_.back();

    // if this decision node should Backtrack.
    // 1. reset implications of decision node.
    // 2. delete all children nodes of decision node.
    // 3. if decision node is propagation node,
    // reset fault observation flag.
    dec->get_imply(imply_good, imply_bad);
    ResetImply(imply_good, imply_bad);
    dec->set_imply(imply_good, imply_bad);

    if (dec->child_) {
      // Delete children of node.
      SplitSiblingTreeNode *child = dec->child_;
      SplitSiblingTreeNode *sibling;
      dec_tree_->delete_silb_child(child);
    }

    if (dec->dec_type() == PROPAGATION && fault_observed_) {
      fault_observed_ = false;
    }

    dec->child_ = nullptr;
    dec->undone_dec();

    // If last node has made all decisions.
    // Delete the node.
    if (!dec->another_dec()) {
      if (dec->dec_type() == GOOD_JUSTIFY || dec->dec_type() == BAD_JUSTIFY) {
        // If parent node is justification node.
        // and if current justification is impossible,
        // reset all sibling nodes, set this node as R flag.
        dynamic_cast<SplitJustifyNode *>(dec)->init();
      } else if (dec->dec_type() == PROPAGATION) {
        dynamic_cast<SplitPropagationNode *>(dec)->init();
      }
      dec_stack_.pop_back();
    }
    // Clear current decision of dec node.
    else {
      assert(dec->last_dec_ < dec->max_dec_);
      return true;
    }
  }

  return false;
}

std::vector<std::pair<Gate *, Gate *>>
SAFTest::PathOfTransitiveFanout(Gate *last_path) {
  std::vector<std::pair<Gate *, Gate *>> prop_dec_pairs;
  std::vector<Gate *> transitive_fanouts;
  std::stack<Gate *> stk;
  std::unordered_set<Gate *> vis;
  if (!OutFaultCone(last_path->GetGId())) {
    stk.emplace(last_path);
    vis.insert(last_path);
  }

  while (!stk.empty()) {
    auto gate = stk.top();
    stk.pop();

    if ((gate->FanoutSize() > 1 || is_observe_gate_[gate->GetGId()]) &&
        (unknown_val(good_[gate->GetGId()]) ||
         unknown_val(bad_[gate->GetGId()]))) {
      transitive_fanouts.emplace_back(gate);
      continue;
    } else if ((is_observe_gate_[gate->GetGId()]) &&
               faulty_val(
                   NINE_VALUE[good_[gate->GetGId()]][bad_[gate->GetGId()]])) {
      if (gate->GetGType() == GType::G_PO) {
        fault_observed_ = true;
        break;
      } else {
        transitive_fanouts.emplace_back(gate->FanoutGates()[0]);
      }
    } else if (!(deter_val(good_[gate->GetGId()]) &&
                 deter_val(bad_[gate->GetGId()]) &&
                 (good_[gate->GetGId()] == bad_[gate->GetGId()]))) {
      for (auto fanout : gate->FanoutGates()) {
        if (!vis.count(fanout) && !OutFaultCone(fanout->GetGId())) {
          stk.emplace(fanout);
          vis.insert(fanout);
        }
      }
    }
  }
  for (auto tf : transitive_fanouts) {
    for (auto fanin : tf->FaninGates()) {
      if (vis.count(fanin)) {
        prop_dec_pairs.emplace_back(fanin, tf);
      }
    }
  }

  return prop_dec_pairs;
}

void SAFTest::EliminateUnjustified(
    std::vector<std::pair<Gate *, uint8_t>> &unjustified, bool is_good) {
  // eliminate all unjustified nodes.
  for (int i = 0; i < unjustified.size();) {
    auto eval = EvalGate(unjustified[i].first, is_good);
    if (eval == unjustified[i].second) {
      swap(unjustified[i], unjustified.back());
      unjustified.pop_back();
    } else {
      i++;
    }
  }
}

void SAFTest::AddToChildrenUnjustified(
    SplitSiblingTreeNode *dec_node,
    std::vector<std::pair<Gate *, uint8_t>> &uj_good,
    std::vector<std::pair<Gate *, uint8_t>> &uj_bad) {
  assert(dec_node);
  std::vector<SplitSiblingTreeNode *> children;
  for (auto item : uj_good) {
    auto new_node =
        new SplitJustifyNode(dec_node, item.first, item.second, true);
    children.emplace_back(dynamic_cast<SplitSiblingTreeNode *>(new_node));
  }
  for (auto item : uj_bad) {
    auto new_node =
        new SplitJustifyNode(dec_node, item.first, item.second, false);
    children.emplace_back(dynamic_cast<SplitSiblingTreeNode *>(new_node));
  }

  dec_tree_->insert_dec(dec_node, children);
}

void SAFTest::AddToChildrenPropagation(SplitSiblingTreeNode *dec_node,
                                       Gate *dec_gate) {
  assert(dec_node);
  auto child = new SplitPropagationNode(dec_node);
  // set all possible path as alternative decisions of child.
  child->gate_ = dec_gate;
  dec_tree_->insert_dec(dec_node, {child});
}

void SAFTest::MergeImplications(std::vector<Gate *> &imply_good,
                                std::vector<Gate *> &imply_bad,
                                std::vector<Gate *> &imply_good_new,
                                std::vector<Gate *> &imply_bad_new) {
  for (auto imply : imply_good) {
    imply_good_new.emplace_back(imply);
  }
  for (auto imply : imply_bad) {
    imply_bad_new.emplace_back(imply);
  }
}


void SAFTest::AddImplicationsToNode(std::vector<Gate *> &imply_good,
                                    std::vector<Gate *> &imply_bad,
                                    SplitSiblingTreeNode *dec_node) {
  std::vector<Gate *> imply_good_origin, imply_bad_origin;
  dec_node->get_imply(imply_good_origin, imply_bad_origin);
  MergeImplications(imply_good, imply_bad, imply_good_origin, imply_bad_origin);
  dec_node->set_imply(imply_good_origin, imply_bad_origin);
}

void SAFTest::ResetImply(std::vector<Gate *> &imply_good,
                         std::vector<Gate *> &imply_bad) {
  while (!imply_good.empty()) {
    auto gate = imply_good.back();
    imply_good.pop_back();
    good_[gate->GetGId()] = LOGIC_x;
  }
  while (!imply_bad.empty()) {
    auto gate = imply_bad.back();
    imply_bad.pop_back();
    bad_[gate->GetGId()] = LOGIC_x;
  }
}


/**
 * @brief
 * backward and forward imply for targeted gate.
 * generate unjustified gates while implying which are potential jusify decison node
 * @param imply_good
 * @param imply_bad
 * @param uj_good
 * @param uj_bad
 */
bool SAFTest::Imply(std::vector<Gate *> &imply_good,
                    std::vector<Gate *> &imply_bad,
                    std::vector<std::pair<Gate *, uint8_t>> &uj_good,
                    std::vector<std::pair<Gate *, uint8_t>> &uj_bad) {
  imply_queue_.clear();
  for (auto imply : imply_good) {
    imply_queue_.emplace_back(imply, true);
  }
  for (auto imply : imply_bad) {
    imply_queue_.emplace_back(imply, false);
  }

  std::pair<Gate *, bool> imply_item;
  while (!imply_queue_.empty()) {
    imply_item = imply_queue_.back();
    imply_queue_.pop_back();

    auto imply_gate = imply_item.first;
    assert(imply_gate != nullptr);

    bool imply_is_good = imply_item.second;

    auto imply_gate_val = GetGateValue(imply_gate, imply_is_good);
    assert(imply_gate_val < LOGIC_x);
    assert(!no_assign_[imply_gate->GetGId()]);

    if (!pre_imply_ &&
        fault_support_region_[gate_ffr_id_[imply_gate->GetGId()]] !=
            atpg_invokes_) {
      continue;
    }
    if (!pre_imply_ && OutFaultCone(imply_gate->GetGId())) {
      if (deter_val(good_[imply_gate->GetGId()]) &&
          deter_val(bad_[imply_gate->GetGId()]) &&
          faulty_val(NINE_VALUE[good_[imply_gate->GetGId()]]
                               [bad_[imply_gate->GetGId()]])) {
        return false;
      }
    }

    if (imply_is_good && prim_->GetClkOffState().count(imply_gate->GetGId()) &&
        imply_gate_val ==
            1 - (int)prim_->GetClkOffState()[imply_gate->GetGId()]) {
      for (auto &clk : prim_->GetClkOffState()) {
        if (clk.first == imply_gate->GetGId()) {
          continue;
        }
        int curr_val = good_[(int)clk.first];
        if (deter_val(curr_val) && curr_val == 1 - (int)clk.second) {
          return false;
        } else if (unknown_val(curr_val)) {
          AssignImplyValue(prim_->GetPrimNetlist()[clk.first], (int)clk.second,
                           true, imply_good, imply_bad, imply_queue_);
        }
      }
    }

    // backwardImply
    GType gate_type = imply_gate->GetGType();
    if (gate_type != GType::G_PI && gate_type != GType::G_TIE0 &&
        gate_type != GType::G_TIE1 && gate_type != GType::G_TIEX &&
        !is_seq_element_[imply_gate->GetGId()] &&
        (imply_is_good || (!pre_imply_ && imply_gate != faulty_gate_))) {
      auto backward_implies =
          BackwardImply(imply_gate, imply_gate_val, imply_is_good);
      // Successfully got backward imply.
      if (backward_implies.size() == 1) {
        auto imply = backward_implies.back();
        // Backward imply conflict.
        if (imply.second.second == LOGIC_CF) {
          return false;
        }
        // Unjustified gate.
        else if (imply.second.second == LOGIC_UJ) {
          if (imply_is_good) {
            uj_good.emplace_back(imply_gate, imply_gate_val);
          } else {
            uj_bad.emplace_back(imply_gate, imply_gate_val);
          }
        } else if (imply.second.first) {
          AssignImplyValue(imply.second.first, imply.second.second, imply.first,
                           imply_good, imply_bad, imply_queue_);
        }
      } else {
        for (auto imply : backward_implies) {
          AssignImplyValue(imply.second.first, imply.second.second, imply.first,
                           imply_good, imply_bad, imply_queue_);
        }
      }
    }

    // forward imply
    uint8_t eval_good;
    uint8_t eval_bad;

    for (auto fanout : imply_gate->FanoutGates()) {
      // stop forward imply when encounter DFF
      if (is_seq_element_[fanout->GetGId()]) {
        continue;
      }
      // if the imply gate is out of cone, fanout is in fault cone
      // because out of cone only have goood value, so need to imply the fanout
      // bad value
      if (!imply_is_good || (OutFaultCone(imply_gate->GetGId()) &&
                             !OutFaultCone(fanout->GetGId()))) {
        if (static_cast<int>(fanout->GetCtrInVal()) ==
            GetGateValue(imply_gate, imply_is_good)) {
          eval_bad = static_cast<int>(fanout->GetCtrOutVal());
        } else {
          eval_bad = EvalGate(fanout, false);
        }

        uint8_t bad_val = bad_[fanout->GetGId()];
        if (unknown_val(bad_val) && eval_bad != bad_val) {
          AssignImplyValue(fanout, eval_bad, false, imply_good, imply_bad,
                           imply_queue_);
        } // fanout may backward imply.
        else if (unknown_val(eval_bad) && deter_val(bad_val)) {
          imply_queue_.emplace_back(fanout, false);
        } else if (deter_val(eval_bad) && deter_val(bad_val) &&
                   eval_bad != bad_val) {
          if (fanout != faulty_gate_) {
            return false;
          }
        }
      }
      if (imply_is_good) {
        if (static_cast<int>(fanout->GetCtrInVal()) ==
            GetGateValue(imply_gate, imply_is_good)) {
          eval_good = static_cast<int>(fanout->GetCtrOutVal());
        } else {
          eval_good = EvalGate(fanout, true);
        }
        uint8_t good_val = good_[fanout->GetGId()];
        if (unknown_val(good_val) && eval_good != good_val) {
          AssignImplyValue(fanout, eval_good, true, imply_good, imply_bad,
                           imply_queue_);
        } else if (unknown_val(eval_good) && deter_val(good_val)) {
          imply_queue_.emplace_back(fanout, true);
        } else if (deter_val(eval_good) && deter_val(good_val) &&
                   eval_good != good_val) {
          return false;
        }
      }
    }
  }

  return true;
}

/**
 * @brief
 * return all possible fanin gate implications
 * @details
 * using driven table to calc cubes
 * @param backward_gate
 * @param backward_val
 * @param backward_gate_isgood_
 * @return
 * 1. conflict
 * 2. unjustified
 * 3. possible cube : <Gate, val>s
 */
std::vector<std::pair<bool, std::pair<Gate *, uint8_t>>>
SAFTest::BackwardImply(Gate *backward_gate, uint8_t backward_val,
                       bool backward_gate_isgood_) {
  int eval_val = EvalGate(backward_gate, backward_gate_isgood_);
  if (deter_val(eval_val) && eval_val != backward_val) {
    return {{true, {nullptr, LOGIC_CF}}};
  } else if (deter_val(eval_val) && eval_val == backward_val) {
    return {{true, {nullptr, LOGIC_x}}};
  } else {
    std::vector<int> fanin_vals;
    for (auto fanin : backward_gate->FaninGates()) {
      bool fanin_is_good = TargetImplyIsGood(fanin, backward_gate_isgood_);
      int fanin_val = GetGateValue(fanin, fanin_is_good);
      fanin_vals.emplace_back(fanin_val);
    }
    auto cubes = driven_table_->possible_cubes(
        backward_gate, backward_val, fanin_vals, gate2scanchainid_,
        is_falling_edge_dff_, no_assign_);
    if (cubes.empty()) {
      return {{true, {nullptr, LOGIC_CF}}};
    }
    if (cubes.size() > 1) {
      return {{true, {nullptr, LOGIC_UJ}}};
    } else if (cubes.size() == 1) {
      std::vector<std::pair<bool, std::pair<Gate *, uint8_t>>> backward_implies;
      for (int fi = 0; fi < backward_gate->FaninSize(); fi++) {
        if (deter_val(cubes[0][fi].second)) {
          Gate *fanin = backward_gate->FaninGates()[fi];
          assert(!no_assign_[fanin->GetGId()]);
          bool fanin_is_good = TargetImplyIsGood(fanin, backward_gate_isgood_);
          int fanin_val = GetGateValue(fanin, fanin_is_good);
          assert(unknown_val(fanin_val));
          backward_implies.emplace_back(
              fanin_is_good, std::make_pair(fanin, cubes[0][fi].second));
        }
      }
      return backward_implies;
    }
  }
  return {{true, {nullptr, LOGIC_x}}};
}

/**
 * @brief
 * set gate value and add it to imply queue
 * @param gate
 * @param val
 * @param is_good
 * @param imply_good
 * @param imply_bad
 * @param imply_queue
 */
void SAFTest::AssignImplyValue(
    Gate *gate, uint8_t val, bool is_good, std::vector<Gate *> &imply_good,
    std::vector<Gate *> &imply_bad,
    std::vector<std::pair<Gate *, bool>> &imply_queue) {
  AssignGateValue(gate, val, is_good);
  if (is_good) {
    imply_good.emplace_back(gate);
  } else {
    imply_bad.emplace_back(gate);
  }
  imply_queue.emplace_back(gate, is_good);
}

/**
 * @brief
 * set gate value in good/bad machine
 * @param gate
 * @param val
 * @param is_good
 */
void SAFTest::AssignGateValue(Gate *gate, uint8_t val, bool is_good) {
  if (pre_imply_)
    assert(is_good);
  assert(!no_assign_[gate->GetGId()]);
  if (is_good) {
    assert(good_[gate->GetGId()] = LOGIC_x);
    good_[gate->GetGId()] = val;
  } else {
    assert(bad_[gate->GetGId()] = LOGIC_x);
    assert(fault_cone_[gate->GetGId()] == atpg_invokes_);
    bad_[gate->GetGId()] = val;
  }
}

/**
 * @brief
 * get gate value from good/bad machine
 * @param gate
 * @param is_good
 * @return current value
 */
int SAFTest::GetGateValue(Gate *gate, bool is_good) {
  return is_good ? good_[gate->GetGId()] : bad_[gate->GetGId()];
}

/**
 * @brief
 * whether current gate use good machine or bad machine
 * @param gate
 * @param is_good
 * @return
 * true if using good machine
 * false if using bad machine
 */
bool SAFTest::TargetImplyIsGood(Gate *gate, bool is_good) {
  return fault_cone_[gate->GetGId()] != atpg_invokes_ || is_good;
}


/**
 * @brief
 * evaluate target gate value according to fanin values
 * @param gate
 * @param is_good
 * @return
 * evaluated value
 */
int SAFTest::EvalGate(Gate *gate, bool is_good) {
  int value;
  int size = gate->FaninSize();
  std::vector<int> &values = is_good ? good_ : bad_;

  GType gate_type = gate->GetGType();
  assert(size > 0 || gate_type == GType::G_PI || gate_type == GType::G_TIE0 ||
         gate_type == GType::G_TIE1);

  auto &fanins = gate->FaninGates();

  switch (gate_type) {
  case GType::G_PI: {
    if (OutFaultCone(gate->GetGId())) {
      value = good_[gate->GetGId()];
    } else {
      value = values[gate->GetGId()];
    }
  } break;
  case GType::G_TIE0:
    value = LOGIC_0;
    break;
  case GType::G_TIE1:
    value = LOGIC_1;
    break;
  case GType::G_BUF:
  case GType::G_PO:
  case GType::G_ABUF:
  case GType::G_BRH: {
    if (OutFaultCone(fanins[0]->GetGId())) {
      value = buf_table_nine[good_[fanins[0]->GetGId()]];
    } else {
      value = buf_table_nine[values[fanins[0]->GetGId()]];
    }
  } break;
  case GType::G_NOT: {
    if (OutFaultCone(fanins[0]->GetGId())) {
      value = not_table_nine[good_[fanins[0]->GetGId()]];
    } else {
      value = not_table_nine[values[fanins[0]->GetGId()]];
    }
  } break;
  case GType::G_AND: {
    if (OutFaultCone(fanins[0]->GetGId())) {
      value = good_[fanins[0]->GetGId()];
    } else {
      value = values[fanins[0]->GetGId()];
    }

    for (int i = 1; i < size; i++) {
      if (OutFaultCone(fanins[i]->GetGId())) {
        value = and_table_nine[value][good_[fanins[i]->GetGId()]];
      } else {
        value = and_table_nine[value][values[fanins[i]->GetGId()]];
      }
    }
  } break;
  case GType::G_NAND: {
    if (OutFaultCone(fanins[0]->GetGId())) {
      value = good_[fanins[0]->GetGId()];
    } else {
      value = values[fanins[0]->GetGId()];
    }

    for (int i = 1; i < size; i++) {
      if (OutFaultCone(fanins[i]->GetGId())) {
        value = and_table_nine[value][good_[fanins[i]->GetGId()]];
      } else {
        value = and_table_nine[value][values[fanins[i]->GetGId()]];
      }
    }
    value = not_table_nine[value];
  } break;
  case GType::G_OR: {
    if (OutFaultCone(fanins[0]->GetGId())) {
      value = good_[fanins[0]->GetGId()];
    } else {
      value = values[fanins[0]->GetGId()];
    }

    for (int i = 1; i < size; i++) {
      if (OutFaultCone(fanins[i]->GetGId())) {
        value = or_table_nine[value][good_[fanins[i]->GetGId()]];
      } else {
        value = or_table_nine[value][values[fanins[i]->GetGId()]];
      }
    }
  } break;
  case GType::G_NOR: {
    if (OutFaultCone(fanins[0]->GetGId())) {
      value = good_[fanins[0]->GetGId()];
    } else {
      value = values[fanins[0]->GetGId()];
    }

    for (int i = 1; i < size; i++) {
      if (OutFaultCone(fanins[i]->GetGId())) {
        value = or_table_nine[value][good_[fanins[i]->GetGId()]];
      } else {
        value = or_table_nine[value][values[fanins[i]->GetGId()]];
      }
    }
    value = not_table_nine[value];
  } break;
  case GType::G_XOR: {
    if (OutFaultCone(fanins[0]->GetGId())) {
      value = good_[fanins[0]->GetGId()];
    } else {
      value = values[fanins[0]->GetGId()];
    }

    for (int i = 1; i < size; i++) {
      if (OutFaultCone(fanins[i]->GetGId())) {
        value = xor_table_nine[value][good_[fanins[i]->GetGId()]];
      } else {
        value = xor_table_nine[value][values[fanins[i]->GetGId()]];
      }
    }
  } break;
  case GType::G_XNOR: {
    if (OutFaultCone(fanins[0]->GetGId())) {
      value = good_[fanins[0]->GetGId()];
    } else {
      value = values[fanins[0]->GetGId()];
    }

    for (int i = 1; i < size; i++) {
      if (OutFaultCone(fanins[i]->GetGId())) {
        value = xor_table_nine[value][good_[fanins[i]->GetGId()]];
      } else {
        value = xor_table_nine[value][values[fanins[i]->GetGId()]];
      }
    }
    value = not_table_nine[value];
  } break;
  case GType::G_MUX: {
    // 0: se, 1: in0, 2: in1.
    uint8_t in0;
    if (OutFaultCone(fanins[1]->GetGId())) {
      in0 = good_[fanins[1]->GetGId()];
    } else {
      in0 = values[fanins[1]->GetGId()];
    }
    uint8_t in1;
    if (OutFaultCone(fanins[2]->GetGId())) {
      in1 = good_[fanins[2]->GetGId()];
    } else {
      in1 = values[fanins[2]->GetGId()];
    }
    uint8_t se;
    if (OutFaultCone(fanins[0]->GetGId())) {
      se = good_[fanins[0]->GetGId()];
    } else {
      se = values[fanins[0]->GetGId()];
    }
    value = or_table_nine[and_table_nine[in0][not_table_nine[se]]]
                         [and_table_nine[in1][se]];

    // se is a reconvergent stem, so X can't hold all conditions.
    if (se == LOGIC_x && in0 == in1) {
      value = in0;
    }
  } break;
  case GType::G_DFF: {
    assert(is_seq_element_[gate->GetGId()]);
    value = LOGIC_x;
    uint8_t set_val = OutFaultCone(fanins[0]->GetGId())
                          ? good_[fanins[0]->GetGId()]
                          : values[fanins[0]->GetGId()];
    uint8_t reset_val = OutFaultCone(fanins[1]->GetGId())
                            ? good_[fanins[1]->GetGId()]
                            : values[fanins[1]->GetGId()];
    uint8_t clk_val = OutFaultCone(fanins[2]->GetGId())
                          ? good_[fanins[2]->GetGId()]
                          : values[fanins[2]->GetGId()];
    uint8_t data_in = OutFaultCone(fanins[3]->GetGId())
                          ? good_[fanins[3]->GetGId()]
                          : values[fanins[3]->GetGId()];
    if (unknown_val(set_val) || unknown_val(reset_val) ||
        unknown_val(clk_val)) {
      value = LOGIC_x;
    } else if (set_val == LOGIC_1 && reset_val == LOGIC_1) {
      LOG_ASSERT(false,
                 "DFF's set and reset cannot be assigend to 1 simultaneously");
    } else if (set_val == LOGIC_1 &&
               clk_val == is_falling_edge_dff_[gate->GetGId()]) {
      value = LOGIC_1;
    } else if (reset_val == LOGIC_1 &&
               clk_val == is_falling_edge_dff_[gate->GetGId()]) {
      value = LOGIC_0;
    } else if (clk_val == 1 - is_falling_edge_dff_[gate->GetGId()]) {
      value = data_in;
    } else {
      value = LOGIC_x;
    }
  } break;
  case GType::G_DLAT: {
    assert(!is_seq_element_[gate->GetGId()]);
    value = LOGIC_x;
    Gate *set = gate->FaninGates()[0];
    Gate *reset = gate->FaninGates()[1];
    Gate *clk = gate->FaninGates()[2];
    Gate *data = gate->FaninGates()[3];
    int set_val = OutFaultCone(set->GetGId()) ? good_[set->GetGId()]
                                              : values[set->GetGId()];
    int reset_val = OutFaultCone(reset->GetGId()) ? good_[reset->GetGId()]
                                                  : values[reset->GetGId()];
    int clk_val = OutFaultCone(clk->GetGId()) ? good_[clk->GetGId()]
                                              : values[clk->GetGId()];
    int data_val = OutFaultCone(data->GetGId()) ? good_[data->GetGId()]
                                                : values[data->GetGId()];
    if (set_val == LOGIC_1 && reset_val == LOGIC_1) {
      assert(false);
    } else if (set_val == LOGIC_1 && reset_val == LOGIC_0 && clk_val == 0) {
      value = LOGIC_1;
    } else if (reset_val == LOGIC_1 && set_val == LOGIC_1 && clk_val == 0) {
      value = LOGIC_0;
    } else if (set_val == LOGIC_0 && reset_val == LOGIC_0 && clk_val == 1) {
      value = data_val;
    } else {
      value = LOGIC_x;
    }
  } break;
  default:
    std::cout << "ERROR: this gate type is not supported!" << std::endl;
    std::cout << static_cast<int>(gate->GetGType()) << std::endl;
    assert(false);
    exit(1);
  }

  return value;
}


 /**
  * @brief
  * whether gate is out of fault effect cone
  * @param gate_id
  * @return
  * true if out of fault effect cone
  * false if in fault effect cone
  */
inline bool SAFTest::OutFaultCone(const int &gate_id) {
  return fault_cone_[gate_id] != atpg_invokes_;
}

} // namespace ictest
